b:, x:Top. if b x else x fi ~ x 

latex

Definitions	Top, Unit, P  Q, P & Q, P  Q, , Prop, b, A, t  T, b, x:A. B(x)
Lemmas	assert wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf